(set-logic QF_UF)
(set-info :source | http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/ |)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(declare-sort U 0)
(declare-sort I 0)
(declare-fun op1 (I I) I)
(declare-fun op (I I) I)
(declare-fun e4 () I)
(declare-fun e3 () I)
(declare-fun e2 () I)
(declare-fun e1 () I)
(declare-fun e0 () I)
(assert (let ((?v_1 (op e0 e0)) (?v_2 (op e0 e1)) (?v_3 (op e0 e2)) (?v_4 (op e0 e3)) (?v_5 (op e0 e4)) (?v_7 (op e1 e0)) (?v_18 (op e1 e1)) (?v_19 (op e1 e2)) (?v_20 (op e1 e3)) (?v_21 (op e1 e4)) (?v_8 (op e2 e0)) (?v_24 (op e2 e1)) (?v_43 (op e2 e2)) (?v_44 (op e2 e3)) (?v_45 (op e2 e4)) (?v_9 (op e3 e0)) (?v_25 (op e3 e1)) (?v_49 (op e3 e2)) (?v_76 (op e3 e3)) (?v_77 (op e3 e4)) (?v_10 (op e4 e0)) (?v_26 (op e4 e1)) (?v_50 (op e4 e2)) (?v_82 (op e4 e3)) (?v_117 (op e4 e4))) (let ((?v_0 (= ?v_1 e0)) (?v_6 (= ?v_1 e1)) (?v_11 (= ?v_1 e2)) (?v_12 (= ?v_1 e3)) (?v_13 (= ?v_1 e4)) (?v_15 (= ?v_2 e0)) (?v_22 (= ?v_2 e1)) (?v_28 (= ?v_2 e2)) (?v_31 (= ?v_2 e3)) (?v_34 (= ?v_2 e4)) (?v_38 (= ?v_3 e0)) (?v_46 (= ?v_3 e1)) (?v_53 (= ?v_3 e2)) (?v_58 (= ?v_3 e3)) (?v_63 (= ?v_3 e4)) (?v_69 (= ?v_4 e0)) (?v_78 (= ?v_4 e1)) (?v_86 (= ?v_4 e2)) (?v_93 (= ?v_4 e3)) (?v_100 (= ?v_4 e4)) (?v_108 (= ?v_5 e0)) (?v_118 (= ?v_5 e1)) (?v_127 (= ?v_5 e2)) (?v_136 (= ?v_5 e3)) (?v_145 (= ?v_5 e4)) (?v_14 (= ?v_7 e0)) (?v_17 (= ?v_7 e1)) (?v_27 (= ?v_7 e2)) (?v_30 (= ?v_7 e3)) (?v_33 (= ?v_7 e4)) (?v_16 (= ?v_18 e0)) (?v_23 (= ?v_18 e1)) (?v_29 (= ?v_18 e2)) (?v_32 (= ?v_18 e3)) (?v_35 (= ?v_18 e4)) (?v_39 (= ?v_19 e0)) (?v_47 (= ?v_19 e1)) (?v_54 (= ?v_19 e2)) (?v_59 (= ?v_19 e3)) (?v_64 (= ?v_19 e4)) (?v_70 (= ?v_20 e0)) (?v_79 (= ?v_20 e1)) (?v_87 (= ?v_20 e2)) (?v_94 (= ?v_20 e3)) (?v_101 (= ?v_20 e4)) (?v_109 (= ?v_21 e0)) (?v_119 (= ?v_21 e1)) (?v_128 (= ?v_21 e2)) (?v_137 (= ?v_21 e3)) (?v_146 (= ?v_21 e4)) (?v_36 (= ?v_8 e0)) (?v_41 (= ?v_8 e1)) (?v_51 (= ?v_8 e2)) (?v_56 (= ?v_8 e3)) (?v_61 (= ?v_8 e4)) (?v_37 (= ?v_24 e0)) (?v_42 (= ?v_24 e1)) (?v_52 (= ?v_24 e2)) (?v_57 (= ?v_24 e3)) (?v_62 (= ?v_24 e4)) (?v_40 (= ?v_43 e0)) (?v_48 (= ?v_43 e1)) (?v_55 (= ?v_43 e2)) (?v_60 (= ?v_43 e3)) (?v_65 (= ?v_43 e4)) (?v_71 (= ?v_44 e0)) (?v_80 (= ?v_44 e1)) (?v_88 (= ?v_44 e2)) (?v_95 (= ?v_44 e3)) (?v_102 (= ?v_44 e4)) (?v_110 (= ?v_45 e0)) (?v_120 (= ?v_45 e1)) (?v_129 (= ?v_45 e2)) (?v_138 (= ?v_45 e3)) (?v_147 (= ?v_45 e4)) (?v_66 (= ?v_9 e0)) (?v_73 (= ?v_9 e1)) (?v_83 (= ?v_9 e2)) (?v_90 (= ?v_9 e3)) (?v_97 (= ?v_9 e4)) (?v_67 (= ?v_25 e0)) (?v_74 (= ?v_25 e1)) (?v_84 (= ?v_25 e2)) (?v_91 (= ?v_25 e3)) (?v_98 (= ?v_25 e4)) (?v_68 (= ?v_49 e0)) (?v_75 (= ?v_49 e1)) (?v_85 (= ?v_49 e2)) (?v_92 (= ?v_49 e3)) (?v_99 (= ?v_49 e4)) (?v_72 (= ?v_76 e0)) (?v_81 (= ?v_76 e1)) (?v_89 (= ?v_76 e2)) (?v_96 (= ?v_76 e3)) (?v_103 (= ?v_76 e4)) (?v_111 (= ?v_77 e0)) (?v_121 (= ?v_77 e1)) (?v_130 (= ?v_77 e2)) (?v_139 (= ?v_77 e3)) (?v_148 (= ?v_77 e4)) (?v_104 (= ?v_10 e0)) (?v_113 (= ?v_10 e1)) (?v_123 (= ?v_10 e2)) (?v_132 (= ?v_10 e3)) (?v_141 (= ?v_10 e4)) (?v_105 (= ?v_26 e0)) (?v_114 (= ?v_26 e1)) (?v_124 (= ?v_26 e2)) (?v_133 (= ?v_26 e3)) (?v_142 (= ?v_26 e4)) (?v_106 (= ?v_50 e0)) (?v_115 (= ?v_50 e1)) (?v_125 (= ?v_50 e2)) (?v_134 (= ?v_50 e3)) (?v_143 (= ?v_50 e4)) (?v_107 (= ?v_82 e0)) (?v_116 (= ?v_82 e1)) (?v_126 (= ?v_82 e2)) (?v_135 (= ?v_82 e3)) (?v_144 (= ?v_82 e4)) (?v_112 (= ?v_117 e0)) (?v_122 (= ?v_117 e1)) (?v_131 (= ?v_117 e2)) (?v_140 (= ?v_117 e3)) (?v_149 (= ?v_117 e4))) (and (and (and (and (and (and (and (and (and (or (or (or (or ?v_0 ?v_15) ?v_38) ?v_69) ?v_108) (or (or (or (or ?v_0 ?v_14) ?v_36) ?v_66) ?v_104)) (and (or (or (or (or ?v_6 ?v_22) ?v_46) ?v_78) ?v_118) (or (or (or (or ?v_6 ?v_17) ?v_41) ?v_73) ?v_113))) (and (or (or (or (or ?v_11 ?v_28) ?v_53) ?v_86) ?v_127) (or (or (or (or ?v_11 ?v_27) ?v_51) ?v_83) ?v_123))) (and (or (or (or (or ?v_12 ?v_31) ?v_58) ?v_93) ?v_136) (or (or (or (or ?v_12 ?v_30) ?v_56) ?v_90) ?v_132))) (and (or (or (or (or ?v_13 ?v_34) ?v_63) ?v_100) ?v_145) (or (or (or (or ?v_13 ?v_33) ?v_61) ?v_97) ?v_141))) (and (and (and (and (and (or (or (or (or ?v_14 ?v_16) ?v_39) ?v_70) ?v_109) (or (or (or (or ?v_15 ?v_16) ?v_37) ?v_67) ?v_105)) (and (or (or (or (or ?v_17 ?v_23) ?v_47) ?v_79) ?v_119) (or (or (or (or ?v_22 ?v_23) ?v_42) ?v_74) ?v_114))) (and (or (or (or (or ?v_27 ?v_29) ?v_54) ?v_87) ?v_128) (or (or (or (or ?v_28 ?v_29) ?v_52) ?v_84) ?v_124))) (and (or (or (or (or ?v_30 ?v_32) ?v_59) ?v_94) ?v_137) (or (or (or (or ?v_31 ?v_32) ?v_57) ?v_91) ?v_133))) (and (or (or (or (or ?v_33 ?v_35) ?v_64) ?v_101) ?v_146) (or (or (or (or ?v_34 ?v_35) ?v_62) ?v_98) ?v_142)))) (and (and (and (and (and (or (or (or (or ?v_36 ?v_37) ?v_40) ?v_71) ?v_110) (or (or (or (or ?v_38 ?v_39) ?v_40) ?v_68) ?v_106)) (and (or (or (or (or ?v_41 ?v_42) ?v_48) ?v_80) ?v_120) (or (or (or (or ?v_46 ?v_47) ?v_48) ?v_75) ?v_115))) (and (or (or (or (or ?v_51 ?v_52) ?v_55) ?v_88) ?v_129) (or (or (or (or ?v_53 ?v_54) ?v_55) ?v_85) ?v_125))) (and (or (or (or (or ?v_56 ?v_57) ?v_60) ?v_95) ?v_138) (or (or (or (or ?v_58 ?v_59) ?v_60) ?v_92) ?v_134))) (and (or (or (or (or ?v_61 ?v_62) ?v_65) ?v_102) ?v_147) (or (or (or (or ?v_63 ?v_64) ?v_65) ?v_99) ?v_143)))) (and (and (and (and (and (or (or (or (or ?v_66 ?v_67) ?v_68) ?v_72) ?v_111) (or (or (or (or ?v_69 ?v_70) ?v_71) ?v_72) ?v_107)) (and (or (or (or (or ?v_73 ?v_74) ?v_75) ?v_81) ?v_121) (or (or (or (or ?v_78 ?v_79) ?v_80) ?v_81) ?v_116))) (and (or (or (or (or ?v_83 ?v_84) ?v_85) ?v_89) ?v_130) (or (or (or (or ?v_86 ?v_87) ?v_88) ?v_89) ?v_126))) (and (or (or (or (or ?v_90 ?v_91) ?v_92) ?v_96) ?v_139) (or (or (or (or ?v_93 ?v_94) ?v_95) ?v_96) ?v_135))) (and (or (or (or (or ?v_97 ?v_98) ?v_99) ?v_103) ?v_148) (or (or (or (or ?v_100 ?v_101) ?v_102) ?v_103) ?v_144)))) (and (and (and (and (and (or (or (or (or ?v_104 ?v_105) ?v_106) ?v_107) ?v_112) (or (or (or (or ?v_108 ?v_109) ?v_110) ?v_111) ?v_112)) (and (or (or (or (or ?v_113 ?v_114) ?v_115) ?v_116) ?v_122) (or (or (or (or ?v_118 ?v_119) ?v_120) ?v_121) ?v_122))) (and (or (or (or (or ?v_123 ?v_124) ?v_125) ?v_126) ?v_131) (or (or (or (or ?v_127 ?v_128) ?v_129) ?v_130) ?v_131))) (and (or (or (or (or ?v_132 ?v_133) ?v_134) ?v_135) ?v_140) (or (or (or (or ?v_136 ?v_137) ?v_138) ?v_139) ?v_140))) (and (or (or (or (or ?v_141 ?v_142) ?v_143) ?v_144) ?v_149) (or (or (or (or ?v_145 ?v_146) ?v_147) ?v_148) ?v_149)))))))
(assert (let ((?v_0 (op e0 e0)) (?v_1 (op e1 e1)) (?v_2 (op e2 e2)) (?v_3 (op e3 e3)) (?v_4 (op e4 e4))) (or (or (or (or (and (and (and (and (not (= ?v_0 e0)) (not (= ?v_1 e0))) (not (= ?v_2 e0))) (not (= ?v_3 e0))) (not (= ?v_4 e0))) (and (and (and (and (not (= ?v_0 e1)) (not (= ?v_1 e1))) (not (= ?v_2 e1))) (not (= ?v_3 e1))) (not (= ?v_4 e1)))) (and (and (and (and (not (= ?v_0 e2)) (not (= ?v_1 e2))) (not (= ?v_2 e2))) (not (= ?v_3 e2))) (not (= ?v_4 e2)))) (and (and (and (and (not (= ?v_0 e3)) (not (= ?v_1 e3))) (not (= ?v_2 e3))) (not (= ?v_3 e3))) (not (= ?v_4 e3)))) (and (and (and (and (not (= ?v_0 e4)) (not (= ?v_1 e4))) (not (= ?v_2 e4))) (not (= ?v_3 e4))) (not (= ?v_4 e4))))))
(assert (let ((?v_25 (op e0 e0)) (?v_27 (op e0 e1)) (?v_29 (op e0 e2)) (?v_31 (op e0 e3)) (?v_33 (op e0 e4)) (?v_28 (op e1 e0)) (?v_37 (op e1 e1)) (?v_39 (op e1 e2)) (?v_41 (op e1 e3)) (?v_43 (op e1 e4)) (?v_30 (op e2 e0)) (?v_40 (op e2 e1)) (?v_49 (op e2 e2)) (?v_51 (op e2 e3)) (?v_53 (op e2 e4)) (?v_32 (op e3 e0)) (?v_42 (op e3 e1)) (?v_52 (op e3 e2)) (?v_61 (op e3 e3)) (?v_63 (op e3 e4)) (?v_34 (op e4 e0)) (?v_44 (op e4 e1)) (?v_54 (op e4 e2)) (?v_64 (op e4 e3)) (?v_73 (op e4 e4))) (let ((?v_0 false) (?v_26 false) (?v_75 false) (?v_100 false) (?v_125 false) (?v_2 false) (?v_36 false) (?v_77 false) (?v_102 false) (?v_127 false) (?v_5 false) (?v_46 false) (?v_80 false) (?v_105 false) (?v_130 false) (?v_10 false) (?v_56 false) (?v_85 false) (?v_110 false) (?v_135 false) (?v_17 false) (?v_66 false) (?v_92 false) (?v_117 false) (?v_142 false) (?v_1 false) (?v_35 false) (?v_76 false) (?v_101 false) (?v_126 false) (?v_3 false) (?v_38 false) (?v_78 false) (?v_103 false) (?v_128 false) (?v_7 false) (?v_48 false) (?v_82 false) (?v_107 false) (?v_132 false) (?v_12 false) (?v_58 false) (?v_87 false) (?v_112 false) (?v_137 false) (?v_19 false) (?v_68 false) (?v_94 false) (?v_119 false) (?v_144 false) (?v_4 false) (?v_45 false) (?v_79 false) (?v_104 false) (?v_129 false) (?v_6 false) (?v_47 false) (?v_81 false) (?v_106 false) (?v_131 false) (?v_8 false) (?v_50 false) (?v_83 false) (?v_108 false) (?v_133 false) (?v_14 false) (?v_60 false) (?v_89 false) (?v_114 false) (?v_139 false) (?v_21 false) (?v_70 false) (?v_96 false) (?v_121 false) (?v_146 false) (?v_9 false) (?v_55 false) (?v_84 false) (?v_109 false) (?v_134 false) (?v_11 false) (?v_57 false) (?v_86 false) (?v_111 false) (?v_136 false) (?v_13 false) (?v_59 false) (?v_88 false) (?v_113 false) (?v_138 false) (?v_15 false) (?v_62 false) (?v_90 false) (?v_115 false) (?v_140 false) (?v_23 false) (?v_72 false) (?v_98 false) (?v_123 false) (?v_148 false) (?v_16 false) (?v_65 false) (?v_91 false) (?v_116 false) (?v_141 false) (?v_18 (= ?v_44 e0)) (?v_67 (= ?v_44 e1)) (?v_93 (= ?v_44 e2)) (?v_118 (= ?v_44 e3)) (?v_143 (= ?v_44 e4)) (?v_20 (= ?v_54 e0)) (?v_69 (= ?v_54 e1)) (?v_95 (= ?v_54 e2)) (?v_120 (= ?v_54 e3)) (?v_145 (= ?v_54 e4)) (?v_22 (= ?v_64 e0)) (?v_71 (= ?v_64 e1)) (?v_97 (= ?v_64 e2)) (?v_122 (= ?v_64 e3)) (?v_147 (= ?v_64 e4)) (?v_24 (= ?v_73 e0)) (?v_74 (= ?v_73 e1)) (?v_99 (= ?v_73 e2)) (?v_124 (= ?v_73 e3)) (?v_149 (= ?v_73 e4))) (and (and (and (and (or (or (or (or (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false false)) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_18))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_20))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_22))) (or (or (or (or (and false false) (and ?v_18 false)) (and ?v_20 false)) (and ?v_22 false)) (and ?v_24 ?v_24))) (or (or (or (or (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false false)) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_67))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_69))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_71))) (or (or (or (or (and false false) (and ?v_67 false)) (and ?v_69 false)) (and ?v_71 false)) (and ?v_74 ?v_74)))) (or (or (or (or (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false false)) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_93))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_95))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_97))) (or (or (or (or (and false false) (and ?v_93 false)) (and ?v_95 false)) (and ?v_97 false)) (and ?v_99 ?v_99)))) (or (or (or (or (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false false)) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_118))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_120))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_122))) (or (or (or (or (and false false) (and ?v_118 false)) (and ?v_120 false)) (and ?v_122 false)) (and ?v_124 ?v_124)))) (or (or (or (or (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_141)) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_143))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_145))) (or (or (or (or (and false false) (and false false)) (and false false)) (and false false)) (and false ?v_147))) (or (or (or (or (and ?v_141 false) (and ?v_143 false)) (and ?v_145 false)) (and ?v_147 false)) (and ?v_149 ?v_149)))))))
(assert (let ((?v_10 (op e0 e3)) (?v_17 (op e0 e4)) (?v_7 (op e1 e2)) (?v_12 (op e1 e3)) (?v_19 (op e1 e4)) (?v_14 (op e2 e3)) (?v_21 (op e2 e4)) (?v_9 (op e3 e0)) (?v_11 (op e3 e1)) (?v_13 (op e3 e2)) (?v_23 (op e3 e4)) (?v_18 (op e4 e1)) (?v_22 (op e4 e3)) (?v_15 (= (op e3 e3) e3))) (or (or (or (or (or (or (and (= ?v_9 e3) (= ?v_10 e3)) (and (= ?v_11 e3) (= ?v_12 e3))) (and (= ?v_13 e3) (= ?v_14 e3))) ?v_15) (and (= ?v_23 e3) (= ?v_22 e3)))) (or (or (or (or (and (= ?v_18 e4) (= ?v_19 e4)))) (and (= ?v_22 e4) (= ?v_23 e4)))))))
(assert (and (= e0 (op e4 e4)) (= e1 (op e0 e0)) (= e2 (op e3 e3)) (= e4 (op e2 e2)) (not (= (op e1 e4) (op e4 e1)))))
(check-sat)
(exit)
